es:event_system{i:l}, L:(Id List), e:es-E(es).
fischer{x:ut2, try:ut2, taken:ut2, contending:ut2, free:ut2, mine:ut2, wanted:ut2, z:ut2}
fischer(es; L)
 f-newround{x:ut2, free:ut2, mine:ut2}
 f-newround(es; L; e)
 f-event{x:ut2}
 f-event(es; L; e) 

latex

Definitions	A, prop{i:l}, t  T, A c B, mkid{$x:ut2}, P  Q, f-event{$x:ut2}(es; L; e), f-newround{$x:ut2, $free:ut2, $mine:ut2}(es; L; e), P  Q, Id, x:A. B(x), False, es-dtype(es; i; x; T), @e(xv)
Lemmas	event system wf, es-E wf, fischer wf, es-when wf, es-change-to wf, es-loc wf, Id wf, l member wf